3.6 Timed Automata (TA) Module

3.6 Timed Automata (TA) Module

Our motivation of Timed Automata (TA) module is to provide a visual environment for users to do model checking. It's based on the theory of timed automata. A timed automaton is a finite-state machine extended with clock variables. All the clocks progress synchronously. In TA module, a system is modeled as a network of several timed automata interleaving with each other. A state of the system is defined by the locations of all automata, the clock constraints, and the values of the global variables. Every automaton may fire an edge (sometimes misleadingly called a transition) separately or synchronise with another automaton, which leads to a new state.